q:. 0  q * q 

latex

Definitions	b, (i = j), qeq(r;s), ff, i <z j, r * s, tt, r + s, r - s, qpositive(r), p q, q_le(r;s), <+>, t.1, , gset, goset, t.2, , x f y, p  q, a < b, if b then t else f fi , b, a <p b, a < b, True, T, False, r < s, {T}, P  Q, P  Q, P  Q, P & Q, P  Q, , t  T, x:A. B(x), A, A c B, Dec(P), S  T
Lemmas	false wf, true wf, squash wf, not wf, decidable qless, decidable cand, decidable equal rationals, decidable or, qless trichot qorder, qminus-positive, and functionality wrt iff, or functionality wrt iff, qmul-non-neg, qmul wf, qless wf, int inc rationals, rationals wf